Nuprl Definition : es-p-local-pred 11,40
es-p-local-pred(es;P)(e,e')
== (e' <loc e) & P(e') & (e'':E. (e'' <loc e)  (e' <loc e'')  ((P(e'')))) 
latex

clarification:

es-p-local-pred(es;P)(e,e')
== es-locl(es; e'; e)
== & P(e')
== & (e'':es-E(es). es-locl(es; e''; e)  es-locl(es; e'; e'')  ((P(e'')))) 
latex

Definitionsx.A(x), P & Q, x:A. B(x), E, P  Q, (e <loc e'), A, f(a)
FDL editor aliaseses-p-local-pred

origin